<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>7. Structures &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="8. Hierarchies" href="C08_Hierarchies.html" />
    <link rel="prev" title="6. Discrete Mathematics" href="C06_Discrete_Mathematics.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">7. Structures</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#defining-structures">7.1. Defining structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#algebraic-structures">7.2. Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#building-the-gaussian-integers">7.3. Building the Gaussian Integers</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">7. </span>Structures</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C07_Structures.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="structures">
<span id="id1"></span><h1><span class="section-number">7. </span>Structures<a class="headerlink" href="#structures" title="Link to this heading">&#61633;</a></h1>
<p>Modern mathematics makes essential use of algebraic
structures,
which encapsulate patterns that can be instantiated in
multiple settings.
The subject provides various ways of defining such structures and
constructing particular instances.</p>
<p>Lean therefore provides corresponding ways of
defining structures formally and working with them.
You have already seen examples of algebraic structures in Lean,
such as rings and lattices, which were discussed in
<a class="reference internal" href="C02_Basics.html#basics"><span class="std std-numref">Chapter 2</span></a>.
This chapter will explain the mysterious square bracket annotations
that you saw there,
<code class="docutils literal notranslate"><span class="pre">[Ring</span> <span class="pre">&#945;]</span></code> and <code class="docutils literal notranslate"><span class="pre">[Lattice</span> <span class="pre">&#945;]</span></code>.
It will also show you how to define and use
algebraic structures on your own.</p>
<p>For more technical detail, you can consult <a class="reference external" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem Proving in Lean</a>,
and a paper by Anne Baanen, <a class="reference external" href="https://arxiv.org/abs/2202.01629">Use and abuse of instance parameters in the Lean mathematical library</a>.</p>
<section id="defining-structures">
<span id="section-structures"></span><h2><span class="section-number">7.1. </span>Defining structures<a class="headerlink" href="#defining-structures" title="Link to this heading">&#61633;</a></h2>
<p>In the broadest sense of the term, a <em>structure</em> is a specification
of a collection of data, possibly with constraints that the
data is required to satisfy.
An <em>instance</em> of the structure is a particular bundle of data satisfying
the constraints. For example, we can specify that a point is
a tuple of three real numbers:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">ext</span><span class="kd">]</span>
<span class="kd">structure</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">&#64;[ext]</span></code> annotation tells Lean to automatically generate theorems
that can be used to prove that two instances of a structure are equal
when their components are equal, a property known as <em>extensionality</em>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Point.ext</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b.x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b.y</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b.z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span>
<span class="w">  </span><span class="n">repeat&#39;</span><span class="w"> </span><span class="n">assumption</span>
</pre></div>
</div>
<p>We can then define particular instances of the <code class="docutils literal notranslate"><span class="pre">Point</span></code> structure.
Lean provides multiple ways of doing that.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myPoint1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">4</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myPoint2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myPoint3</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Point.mk</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="mi">4</span>
</pre></div>
</div>
<p>In the first example, the fields of the structure are named
explicitly.
The function <code class="docutils literal notranslate"><span class="pre">Point.mk</span></code> referred to in the definition of <code class="docutils literal notranslate"><span class="pre">myPoint3</span></code>
is known as the <em>constructor</em> for the <code class="docutils literal notranslate"><span class="pre">Point</span></code> structure, because
it serves to construct elements.
You can specify a different name if you want, like <code class="docutils literal notranslate"><span class="pre">build</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">Point&#39;</span><span class="w"> </span><span class="n">where</span><span class="w"> </span><span class="n">build</span><span class="w"> </span><span class="o">::</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Point&#39;.build</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="mi">4</span>
</pre></div>
</div>
<p>The next two examples show how to define functions on structures.
Whereas the second example makes the <code class="docutils literal notranslate"><span class="pre">Point.mk</span></code>
constructor explicit, the first example uses an anonymous constructor
for brevity.
Lean can infer the relevant constructor from the indicated type of
<code class="docutils literal notranslate"><span class="pre">add</span></code>.
It is conventional to put definitions and theorems associated
with a structure like <code class="docutils literal notranslate"><span class="pre">Point</span></code> in a namespace with the same name.
In the example below, because we have opened the <code class="docutils literal notranslate"><span class="pre">Point</span></code>
namespace, the full name of <code class="docutils literal notranslate"><span class="pre">add</span></code> is <code class="docutils literal notranslate"><span class="pre">Point.add</span></code>.
When the namespace is not open, we have to use the full name.
But remember that it is often convenient to use
anonymous projection notation,
which allows us to write <code class="docutils literal notranslate"><span class="pre">a.add</span> <span class="pre">b</span></code> instead of <code class="docutils literal notranslate"><span class="pre">Point.add</span> <span class="pre">a</span> <span class="pre">b</span></code>.
Lean interprets the former as the latter because <code class="docutils literal notranslate"><span class="pre">a</span></code> has type <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">namespace</span><span class="w"> </span><span class="n">Point</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="o">,</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span><span class="o">,</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span>

<span class="k">#check</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">myPoint1</span><span class="w"> </span><span class="n">myPoint2</span>
<span class="k">#check</span><span class="w"> </span><span class="n">myPoint1.add</span><span class="w"> </span><span class="n">myPoint2</span>

<span class="kd">end</span><span class="w"> </span><span class="n">Point</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Point.add</span><span class="w"> </span><span class="n">myPoint1</span><span class="w"> </span><span class="n">myPoint2</span>
<span class="k">#check</span><span class="w"> </span><span class="n">myPoint1.add</span><span class="w"> </span><span class="n">myPoint2</span>
</pre></div>
</div>
<p>Below we will continue to put definitions in the relevant
namespace, but we will leave the namespacing commands out of the quoted
snippets. To prove properties of the addition function,
we can use <code class="docutils literal notranslate"><span class="pre">rw</span></code> to expand the definition and <code class="docutils literal notranslate"><span class="pre">ext</span></code> to
reduce an equation between two elements of the structure to equations
between the components.
Below we use the <code class="docutils literal notranslate"><span class="pre">protected</span></code> keyword so that the name of the
theorem is <code class="docutils literal notranslate"><span class="pre">Point.add_comm</span></code>, even when the namespace is open.
This is helpful when we want to avoid ambiguity with a generic
theorem like <code class="docutils literal notranslate"><span class="pre">add_comm</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">protected</span><span class="w"> </span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">add</span><span class="o">]</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">dsimp</span>
<span class="w">  </span><span class="n">repeat&#39;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">add_comm</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>Because Lean can unfold definitions and simplify projections
internally, sometimes the equations we want hold definitionally.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_x</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a.add</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">.</span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It is also possible to define functions on structures using
pattern matching,
in a manner similar to the way we defined recursive functions in
<a class="reference internal" href="C05_Elementary_Number_Theory.html#section-induction-and-recursion"><span class="std std-numref">Section 5.2</span></a>.
The definitions <code class="docutils literal notranslate"><span class="pre">addAlt</span></code> and <code class="docutils literal notranslate"><span class="pre">addAlt'</span></code> below are essentially the
same; the only difference is that we use anonymous constructor notation
in the second.
Although it is sometimes convenient to define functions this way, and structural eta-reduction makes
this alternative definitionally equivalent, it can make things less convenient in later proofs.
In particular, <code class="docutils literal notranslate"><span class="pre">rw</span> <span class="pre">[addAlt]</span></code> leaves us with a messier goal view containing a <code class="docutils literal notranslate"><span class="pre">match</span></code> statement.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">addAlt</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">Point.mk</span><span class="w"> </span><span class="n">x&#8321;</span><span class="w"> </span><span class="n">y&#8321;</span><span class="w"> </span><span class="n">z&#8321;</span><span class="o">,</span><span class="w"> </span><span class="n">Point.mk</span><span class="w"> </span><span class="n">x&#8322;</span><span class="w"> </span><span class="n">y&#8322;</span><span class="w"> </span><span class="n">z&#8322;</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">z&#8322;</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">addAlt&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8321;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8321;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8321;</span><span class="o">&#10217;,</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8322;</span><span class="o">&#10217;</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">z&#8322;</span><span class="o">&#10217;</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">addAlt_x</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a.addAlt</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">.</span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">addAlt_comm</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">addAlt</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">addAlt</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">addAlt</span><span class="o">,</span><span class="w"> </span><span class="n">addAlt</span><span class="o">]</span>
<span class="w">  </span><span class="c1">-- the same proof still works, but the goal view here is harder to read</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">dsimp</span>
<span class="w">  </span><span class="n">repeat&#39;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">add_comm</span>
</pre></div>
</div>
<p>Mathematical constructions often involve taking apart bundled information and
putting it together again in different ways.
It therefore makes sense that Lean and Mathlib offer so many ways
of doing this efficiently.
As an exercise, try proving that <code class="docutils literal notranslate"><span class="pre">Point.add</span></code> is associative.
Then define scalar multiplication for a point and show that it
distributes over addition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">protected</span><span class="w"> </span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a.add</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">.</span><span class="n">add</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a.add</span><span class="w"> </span><span class="o">(</span><span class="n">b.add</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">def</span><span class="w"> </span><span class="n">smul</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">smul_distrib</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="bp">.</span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">(</span><span class="n">a.add</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Using structures is only the first step on the road to
algebraic abstraction.
We don&#8217;t yet have a way to link <code class="docutils literal notranslate"><span class="pre">Point.add</span></code> to the generic <code class="docutils literal notranslate"><span class="pre">+</span></code> symbol,
or to connect <code class="docutils literal notranslate"><span class="pre">Point.add_comm</span></code> and <code class="docutils literal notranslate"><span class="pre">Point.add_assoc</span></code> to
the generic <code class="docutils literal notranslate"><span class="pre">add_comm</span></code> and <code class="docutils literal notranslate"><span class="pre">add_assoc</span></code> theorems.
These tasks belong to the <em>algebraic</em> aspect of using structures,
and we will explain how to carry them out in the next section.
For now, just think of a structure as a way of bundling together objects
and information.</p>
<p>It is especially useful that a structure can specify not only
data types but also constraints that the data must satisfy.
In Lean, the latter are represented as fields of type <code class="docutils literal notranslate"><span class="pre">Prop</span></code>.
For example, the <em>standard 2-simplex</em> is defined to be the set of
points <span class="math notranslate nohighlight">\((x, y, z)\)</span> satisfying <span class="math notranslate nohighlight">\(x &#8805; 0\)</span>, <span class="math notranslate nohighlight">\(y &#8805; 0\)</span>, <span class="math notranslate nohighlight">\(z &#8805; 0\)</span>,
and <span class="math notranslate nohighlight">\(x + y + z = 1\)</span>.
If you are not familiar with the notion, you should draw a picture,
and convince yourself that this set is
the equilateral triangle in three-space with vertices
<span class="math notranslate nohighlight">\((1, 0, 0)\)</span>, <span class="math notranslate nohighlight">\((0, 1, 0)\)</span>, and <span class="math notranslate nohighlight">\((0, 0, 1)\)</span>,
together with its interior.
We can represent it in Lean as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">x_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">y_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span>
<span class="w">  </span><span class="n">z_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span>
<span class="w">  </span><span class="n">sum_eq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span>
</pre></div>
</div>
<p>Notice that the last four fields refer to <code class="docutils literal notranslate"><span class="pre">x</span></code>, <code class="docutils literal notranslate"><span class="pre">y</span></code>, and <code class="docutils literal notranslate"><span class="pre">z</span></code>,
that is, the first three fields.
We can define a map from the two-simplex to itself that swaps <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">swapXy</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.y</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.x</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.z</span>
<span class="w">  </span><span class="n">x_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.y_nonneg</span>
<span class="w">  </span><span class="n">y_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.x_nonneg</span>
<span class="w">  </span><span class="n">z_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.z_nonneg</span>
<span class="w">  </span><span class="n">sum_eq</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="n">a.x</span><span class="o">,</span><span class="w"> </span><span class="n">a.sum_eq</span><span class="o">]</span>
</pre></div>
</div>
<p>More interestingly, we can compute the midpoint of two points on
the simplex. We have added the phrase <code class="docutils literal notranslate"><span class="pre">noncomputable</span> <span class="pre">section</span></code>
at the beginning of this file in order to use division on the real numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span>

<span class="kd">def</span><span class="w"> </span><span class="n">midpoint</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">x_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">div_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="n">a.x_nonneg</span><span class="w"> </span><span class="n">b.x_nonneg</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">y_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">div_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="n">a.y_nonneg</span><span class="w"> </span><span class="n">b.y_nonneg</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">z_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">div_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="n">a.z_nonneg</span><span class="w"> </span><span class="n">b.z_nonneg</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">sum_eq</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">field_simp</span><span class="bp">;</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">a.sum_eq</span><span class="o">,</span><span class="w"> </span><span class="n">b.sum_eq</span><span class="o">]</span>
</pre></div>
</div>
<p>Here we have established <code class="docutils literal notranslate"><span class="pre">x_nonneg</span></code>, <code class="docutils literal notranslate"><span class="pre">y_nonneg</span></code>, and <code class="docutils literal notranslate"><span class="pre">z_nonneg</span></code>
with concise proof terms, but establish <code class="docutils literal notranslate"><span class="pre">sum_eq</span></code> in tactic mode,
using <code class="docutils literal notranslate"><span class="pre">by</span></code>.</p>
<p>Given a parameter <span class="math notranslate nohighlight">\(\lambda\)</span> satisfying <span class="math notranslate nohighlight">\(0 \le \lambda \le 1\)</span>,
we can take the weighted average <span class="math notranslate nohighlight">\(\lambda a + (1 - \lambda) b\)</span>
of two points <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> in the standard 2-simplex.
We challenge you to define that function, in analogy to the <code class="docutils literal notranslate"><span class="pre">midpoint</span></code>
function above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">weightedAverage</span><span class="w"> </span><span class="o">(</span><span class="n">lambda</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Real</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">lambda_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">lambda</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">lambda_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">lambda</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Structures can depend on parameters.
For example, we can generalize the standard 2-simplex to the standard
<span class="math notranslate nohighlight">\(n\)</span>-simplex for any <span class="math notranslate nohighlight">\(n\)</span>.
At this stage, you don&#8217;t have to know anything about the type <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">n</span></code>
except that it has <span class="math notranslate nohighlight">\(n\)</span> elements, and that Lean knows
how to sum over it.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">BigOperators</span>

<span class="kd">structure</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">NonNeg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span>
<span class="w">  </span><span class="n">sum_eq_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span>

<span class="kn">namespace</span><span class="w"> </span><span class="n">StandardSimplex</span>

<span class="kd">def</span><span class="w"> </span><span class="n">midpoint</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">NonNeg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">i</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">div_nonneg</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">a.NonNeg</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">b.NonNeg</span><span class="w"> </span><span class="n">i</span><span class="o">]</span>
<span class="w">    </span><span class="n">norm_num</span>
<span class="w">  </span><span class="n">sum_eq_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">div_eq_mul_inv</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">Finset.sum_mul</span><span class="o">,</span><span class="w"> </span><span class="n">Finset.sum_add_distrib</span><span class="o">,</span>
<span class="w">      </span><span class="n">a.sum_eq_one</span><span class="o">,</span><span class="w"> </span><span class="n">b.sum_eq_one</span><span class="o">]</span>
<span class="w">    </span><span class="n">field_simp</span>

<span class="kd">end</span><span class="w"> </span><span class="n">StandardSimplex</span>
</pre></div>
</div>
<p>As an exercise, see if you can define the weighted average of
two points in the standard <span class="math notranslate nohighlight">\(n\)</span>-simplex.
You can use <code class="docutils literal notranslate"><span class="pre">Finset.sum_add_distrib</span></code>
and <code class="docutils literal notranslate"><span class="pre">Finset.mul_sum</span></code> to manipulate the relevant sums.</p>
<p>We have seen that structures can be used to bundle together data
and properties.
Interestingly, they can also be used to bundle together properties
without the data.
For example, the next structure, <code class="docutils literal notranslate"><span class="pre">IsLinear</span></code>, bundles together
the two components of linearity.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">IsLinear</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">is_additive</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span>
<span class="w">  </span><span class="n">preserves_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">linf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsLinear</span><span class="w"> </span><span class="n">f</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">linf.is_additive</span>
<span class="k">#check</span><span class="w"> </span><span class="n">linf.preserves_mul</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>It is worth pointing out that structures are not the only way to bundle
together data.
The <code class="docutils literal notranslate"><span class="pre">Point</span></code> data structure can be defined using the generic type product,
and <code class="docutils literal notranslate"><span class="pre">IsLinear</span></code> can be defined with a simple <code class="docutils literal notranslate"><span class="pre">and</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">Point&#39;&#39;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">IsLinear&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>Generic type constructions can even be used in place of structures
with dependencies between their components.
For example, the <em>subtype</em> construction combines a piece of data with
a property.
You can think of the type <code class="docutils literal notranslate"><span class="pre">PReal</span></code> in the next example as being
the type of positive real numbers.
Any <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">:</span> <span class="pre">PReal</span></code> has two components: the value, and the property of being
positive.
You can access these components as <code class="docutils literal notranslate"><span class="pre">x.val</span></code>, which has type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>,
and <code class="docutils literal notranslate"><span class="pre">x.property</span></code>, which represents the fact <code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">x.val</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">PReal</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">}</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">PReal</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">x.val</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x.property</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="bp">.</span><span class="mi">1</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="bp">.</span><span class="mi">2</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>We could have used subtypes to define the standard 2-simplex,
as well as the standard <span class="math notranslate nohighlight">\(n\)</span>-simplex for an arbitrary <span class="math notranslate nohighlight">\(n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">StandardTwoSimplex&#39;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">}</span>

<span class="kd">def</span><span class="w"> </span><span class="n">StandardSimplex&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">}</span>
</pre></div>
</div>
<p>Similarly, <em>Sigma types</em> are generalizations of ordered pairs,
whereby the type of the second component depends on the type of
the first.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">StdSimplex</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">&#931;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="n">n</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StdSimplex</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">s.fst</span>
<span class="k">#check</span><span class="w"> </span><span class="n">s.snd</span>

<span class="k">#check</span><span class="w"> </span><span class="n">s</span><span class="bp">.</span><span class="mi">1</span>
<span class="k">#check</span><span class="w"> </span><span class="n">s</span><span class="bp">.</span><span class="mi">2</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>Given <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">StdSimplex</span></code>, the first component <code class="docutils literal notranslate"><span class="pre">s.fst</span></code> is a natural
number, and the second component is an element of the corresponding
simplex <code class="docutils literal notranslate"><span class="pre">StandardSimplex</span> <span class="pre">s.fst</span></code>.
The difference between a Sigma type and a subtype is that
the second component of a Sigma type is data rather than a proposition.</p>
<p>But even though we can use products, subtypes, and Sigma types
instead of structures, using structures has a number of advantages.
Defining a structure abstracts away the underlying representation
and provides custom names for the functions that access the components.
This makes proofs more robust:
proofs that rely only on the interface to a structure
will generally continue to work when we change the definition,
as long as we redefine the old accessors in terms of the new definition.
Moreover, as we are about to see, Lean provides support for
weaving structures together into a rich, interconnected hierarchy,
and for managing the interactions between them.</p>
</section>
<section id="algebraic-structures">
<span id="section-algebraic-structures"></span><h2><span class="section-number">7.2. </span>Algebraic Structures<a class="headerlink" href="#algebraic-structures" title="Link to this heading">&#61633;</a></h2>
<p>To clarify what we mean by the phrase <em>algebraic structure</em>,
it will help to consider some examples.</p>
<ol class="arabic simple">
<li><p>A <em>partially ordered set</em> consists of a set <span class="math notranslate nohighlight">\(P\)</span> and
a binary relation <span class="math notranslate nohighlight">\(\le\)</span> on <span class="math notranslate nohighlight">\(P\)</span> that is transitive
and reflexive.</p></li>
<li><p>A <em>group</em> consists of a set <span class="math notranslate nohighlight">\(G\)</span> with an associative
binary operation, an identity element
<span class="math notranslate nohighlight">\(1\)</span>, and a function <span class="math notranslate nohighlight">\(g \mapsto g^{-1}\)</span> that returns
an inverse for each <span class="math notranslate nohighlight">\(g\)</span> in <span class="math notranslate nohighlight">\(G\)</span>.
A group is <em>abelian</em> or <em>commutative</em> if the operation is commutative.</p></li>
<li><p>A <em>lattice</em> is a partially ordered set with meets and joins.</p></li>
<li><p>A <em>ring</em> consists of an (additively written) abelian group
<span class="math notranslate nohighlight">\((R, +, 0, x \mapsto -x)\)</span>
together with an associative multiplication operation
<span class="math notranslate nohighlight">\(\cdot\)</span> and an identity <span class="math notranslate nohighlight">\(1\)</span>,
such that multiplication distributes over addition.
A ring is <em>commutative</em> if the multiplication is commutative.</p></li>
<li><p>An <em>ordered ring</em> <span class="math notranslate nohighlight">\((R, +, 0, -, \cdot, 1, \le)\)</span> consists of a ring
together with a partial order on its elements, such that <span class="math notranslate nohighlight">\(a \le b\)</span> implies
<span class="math notranslate nohighlight">\(a + c \le b + c\)</span> for every <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, and <span class="math notranslate nohighlight">\(c\)</span> in <span class="math notranslate nohighlight">\(R\)</span>,
and <span class="math notranslate nohighlight">\(0 \le a\)</span> and <span class="math notranslate nohighlight">\(0 \le b\)</span> implies <span class="math notranslate nohighlight">\(0 \le a b\)</span> for
every <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> in <span class="math notranslate nohighlight">\(R\)</span>.</p></li>
<li><p>A <em>metric space</em> consists of a set <span class="math notranslate nohighlight">\(X\)</span> and a function
<span class="math notranslate nohighlight">\(d : X \times X \to \mathbb{R}\)</span> such that the following hold:</p>
<ul class="simple">
<li><p><span class="math notranslate nohighlight">\(d(x, y) \ge 0\)</span> for every <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> in <span class="math notranslate nohighlight">\(X\)</span>.</p></li>
<li><p><span class="math notranslate nohighlight">\(d(x, y) = 0\)</span> if and only if <span class="math notranslate nohighlight">\(x = y\)</span>.</p></li>
<li><p><span class="math notranslate nohighlight">\(d(x, y) = d(y, x)\)</span> for every <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> in <span class="math notranslate nohighlight">\(X\)</span>.</p></li>
<li><p><span class="math notranslate nohighlight">\(d(x, z) \le d(x, y) + d(y, z)\)</span> for every <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(y\)</span>, and
<span class="math notranslate nohighlight">\(z\)</span> in <span class="math notranslate nohighlight">\(X\)</span>.</p></li>
</ul>
</li>
<li><p>A <em>topological space</em> consists of a set <span class="math notranslate nohighlight">\(X\)</span> and a collection <span class="math notranslate nohighlight">\(\mathcal T\)</span>
of subsets of <span class="math notranslate nohighlight">\(X\)</span>, called the <em>open subsets of</em> <span class="math notranslate nohighlight">\(X\)</span>, such that
the following hold:</p>
<ul class="simple">
<li><p>The empty set and <span class="math notranslate nohighlight">\(X\)</span> are open.</p></li>
<li><p>The intersection of two open sets is open.</p></li>
<li><p>An arbitrary union of open sets is open.</p></li>
</ul>
</li>
</ol>
<p>In each of these examples, the elements of the structure belong to a
set, the <em>carrier set</em>,
that sometimes stands proxy for the entire structure.
For example, when we say &#8220;let <span class="math notranslate nohighlight">\(G\)</span> be a group&#8221; and then
&#8220;let <span class="math notranslate nohighlight">\(g \in G\)</span>,&#8221; we are using <span class="math notranslate nohighlight">\(G\)</span> to stand for both
the structure and its carrier.
Not every algebraic structure is associated with a single carrier set in this way.
For example, a <em>bipartite graph</em> involves a relation between two sets,
as does a <em>Galois connection</em>,
A <em>category</em> also involves two sets of interest, commonly called the <em>objects</em>
and the <em>morphisms</em>.</p>
<p>The examples indicate some of the things that a proof assistant has to do
in order to support algebraic reasoning.
First, it needs to recognize concrete instances of structures.
The number systems <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>,
and <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> are all ordered rings,
and we should be able to apply a generic theorem about ordered rings
in any of these instances.
Sometimes a concrete set may be an instance of a structure in more than one way.
For example, in addition to the usual topology on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>,
which forms the basis for real analysis,
we can also consider the <em>discrete</em> topology on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>,
in which every set is open.</p>
<p>Second, a proof assistant needs to support generic notation on structures.
In Lean, the notation <code class="docutils literal notranslate"><span class="pre">*</span></code>
is used for multiplication in all the usual number systems,
as well as for multiplication in generic groups and rings.
When we use an expression like <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span></code>,
Lean has to use information about the types of <code class="docutils literal notranslate"><span class="pre">f</span></code>, <code class="docutils literal notranslate"><span class="pre">x</span></code>, and <code class="docutils literal notranslate"><span class="pre">y</span></code>
to determine which multiplication we have in mind.</p>
<p>Third, it needs to deal with the fact that structures can inherit
definitions, theorems, and notation from other structures in various ways.
Some structures extend others by adding more axioms.
A commutative ring is still a ring, so any definition
that makes sense in a ring also makes sense in a commutative ring,
and any theorem that holds in a ring also holds in a commutative ring.
Some structures extend others by adding more data.
For example, the additive part of any ring is an additive group.
The ring structure adds a multiplication and an identity,
as well as axioms that govern them and relate them to the additive part.
Sometimes we can define one structure in terms of another.
Any metric space has a canonical topology associated with it,
the <em>metric space topology</em>, and there are various topologies that can be
associated with any linear ordering.</p>
<p>Finally, it is important to keep in mind that mathematics allows us to
use functions and operations to define structures in the same way we
use functions and operations to define numbers.
Products and powers of groups are again groups.
For every <span class="math notranslate nohighlight">\(n\)</span>, the integers modulo <span class="math notranslate nohighlight">\(n\)</span> form a ring,
and for every <span class="math notranslate nohighlight">\(k &gt; 0\)</span>, the <span class="math notranslate nohighlight">\(k \times k\)</span> matrices of polynomials
with coefficients in that ring again form a ring.
Thus we can calculate with structures just as easily as we can calculate
with their elements.
This means that algebraic structures lead dual lives in mathematics,
as containers for collections of objects and as objects in their own right.
A proof assistant has to accommodate this dual role.</p>
<p>When dealing with elements of a type that has an algebraic structure
associated with it,
a proof assistant needs to recognize the structure and find the relevant
definitions, theorems, and notation.
All this should sound like a lot of work, and it is.
But Lean uses a small collection of fundamental mechanisms to
carry out these tasks.
The goal of this section is to explain these mechanisms and show you
how to use them.</p>
<p>The first ingredient is almost too obvious to mention:
formally speaking, algebraic structures are structures in the sense
of <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a>.
An algebraic structure is a specification of a bundle of data satisfying
some axiomatic hypotheses, and we saw in <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a> that
this is exactly what the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command is designed to accommodate.
It&#8217;s a marriage made in heaven!</p>
<p>Given a data type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, we can define the group structure on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>
as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">Group&#8321;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">inv</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">one</span>
</pre></div>
</div>
<p>Notice that the type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is a <em>parameter</em> in the definition of <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code>.
So you should think of an object <code class="docutils literal notranslate"><span class="pre">struc</span> <span class="pre">:</span> <span class="pre">Group&#8321;</span> <span class="pre">&#945;</span></code> as being
a group structure on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
We saw in <a class="reference internal" href="C02_Basics.html#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a>
that the counterpart <code class="docutils literal notranslate"><span class="pre">mul_inv_cancel</span></code> to <code class="docutils literal notranslate"><span class="pre">inv_mul_cancel</span></code>
follows from the other group axioms, so there is no need
to add it to the definition.</p>
<p>This definition of a group is similar to the definition of <code class="docutils literal notranslate"><span class="pre">Group</span></code> in
Mathlib,
and we have chosen the name <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> to distinguish our version.
If you write <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">Group</span></code> and ctrl-click on the definition,
you will see that the Mathlib version of <code class="docutils literal notranslate"><span class="pre">Group</span></code> is defined to
extend another structure; we will explain how to do that later.
If you type <code class="docutils literal notranslate"><span class="pre">#print</span> <span class="pre">Group</span></code> you will also see that the Mathlib
version of <code class="docutils literal notranslate"><span class="pre">Group</span></code> has a number of extra fields.
For reasons we will explain later, sometimes it is useful to add
redundant information to a structure,
so that there are additional fields for objects and functions
that can be defined from the core
data. Don&#8217;t worry about that for now.
Rest assured that our simplified version <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> is
morally the same as the definition of a group that Mathlib uses.</p>
<p>It is sometimes useful to bundle
the type together with the structure, and Mathlib also
contains a definition of a <code class="docutils literal notranslate"><span class="pre">Grp</span></code> structure that is equivalent to
the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">Grp&#8321;</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span>
<span class="w">  </span><span class="n">str</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8321;</span><span class="w"> </span><span class="n">&#945;</span>
</pre></div>
</div>
<p>The Mathlib version is found in <code class="docutils literal notranslate"><span class="pre">Mathlib.Algebra.Category.Grp.Basic</span></code>,
and you can <code class="docutils literal notranslate"><span class="pre">#check</span></code> it if you add this to the imports at the
beginning of the examples file.</p>
<p>For reasons that will become clearer below, it is more often
useful to keep the type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> separate from the structure <code class="docutils literal notranslate"><span class="pre">Group</span> <span class="pre">&#945;</span></code>.
We refer to the two objects together as a <em>partially bundled structure</em>,
since the representation combines most, but not all, of the components
into one structure. It is common in Mathlib
to use capital roman letters like <code class="docutils literal notranslate"><span class="pre">G</span></code> for a type
when it is used as the carrier type for a group.</p>
<p>Let&#8217;s construct a group, which is to say, an element of the <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> type.
For any pair of types <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>, Mathlib defines the type <code class="docutils literal notranslate"><span class="pre">Equiv</span> <span class="pre">&#945;</span> <span class="pre">&#946;</span></code>
of <em>equivalences</em> between <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>.
Mathlib also defines the suggestive notation <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">&#8771;</span> <span class="pre">&#946;</span></code> for this type.
An element <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#945;</span> <span class="pre">&#8771;</span> <span class="pre">&#946;</span></code> is a bijection between <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>
represented by four components:
a function <code class="docutils literal notranslate"><span class="pre">f.toFun</span></code> from <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>,
the inverse function <code class="docutils literal notranslate"><span class="pre">f.invFun</span></code> from <code class="docutils literal notranslate"><span class="pre">&#946;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>,
and two properties that specify these functions are indeed inverse
to one another.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="n">&#947;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#946;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#947;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Equiv</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="n">&#946;</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.toFun</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#946;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.invFun</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.right_inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f.invFun</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.left_inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">f.invFun</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.symm</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#947;</span><span class="o">)</span>
</pre></div>
</div>
<p>Notice the creative naming of the last three constructions. We think of the
identity function <code class="docutils literal notranslate"><span class="pre">Equiv.refl</span></code>, the inverse operation <code class="docutils literal notranslate"><span class="pre">Equiv.symm</span></code>,
and the composition operation <code class="docutils literal notranslate"><span class="pre">Equiv.trans</span></code> as explicit evidence
that the property of being in bijective correspondence is an equivalence relation.</p>
<p>Notice also that <code class="docutils literal notranslate"><span class="pre">f.trans</span> <span class="pre">g</span></code> requires composing the forward functions
in reverse order. Mathlib has declared a <em>coercion</em> from <code class="docutils literal notranslate"><span class="pre">Equiv</span> <span class="pre">&#945;</span> <span class="pre">&#946;</span></code>
to the function type <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">&#8594;</span> <span class="pre">&#946;</span></code>, so we can omit writing <code class="docutils literal notranslate"><span class="pre">.toFun</span></code>
and have Lean insert it for us.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="bp">.</span><span class="n">toFun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g.toFun</span><span class="w"> </span><span class="o">(</span><span class="n">f.toFun</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#947;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8728;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>Mathlib also defines the type <code class="docutils literal notranslate"><span class="pre">perm</span> <span class="pre">&#945;</span></code> of equivalences between
<code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and itself.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It should be clear that <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code> forms a group under composition
of equivalences. We orient things so that <code class="docutils literal notranslate"><span class="pre">mul</span> <span class="pre">f</span> <span class="pre">g</span></code> is
equal to <code class="docutils literal notranslate"><span class="pre">g.trans</span> <span class="pre">f</span></code>, whose forward function is <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">&#8728;</span> <span class="pre">g</span></code>.
In other words, multiplication is what we ordinarily think of as
composition of the bijections. Here we define this group:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">permGroup</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8321;</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">f</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.symm</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.trans_assoc</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans_refl</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl_trans</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.self_trans_symm</span>
</pre></div>
</div>
<p>In fact, Mathlib defines exactly this <code class="docutils literal notranslate"><span class="pre">Group</span></code> structure on <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code>
in the file <code class="docutils literal notranslate"><span class="pre">Algebra.Group.End</span></code>.
As always, you can hover over the theorems used in the definition of
<code class="docutils literal notranslate"><span class="pre">permGroup</span></code> to see their statements,
and you can jump to their definitions in the original file to learn
more about how they are implemented.</p>
<p>In ordinary mathematics, we generally think of notation as
independent of structure.
For example, we can consider groups <span class="math notranslate nohighlight">\((G_1, \cdot, 1, \cdot^{-1})\)</span>,
<span class="math notranslate nohighlight">\((G_2, \circ, e, i(\cdot))\)</span>, and <span class="math notranslate nohighlight">\((G_3, +, 0, -)\)</span>.
In the first case, we write the binary operation as <span class="math notranslate nohighlight">\(\cdot\)</span>,
the identity as <span class="math notranslate nohighlight">\(1\)</span>, and the inverse function as <span class="math notranslate nohighlight">\(x \mapsto x^{-1}\)</span>.
In the second and third cases, we use the notational alternatives shown.
When we formalize the notion of a group in Lean, however,
the notation is more tightly linked to the structure.
In Lean, the components of any <code class="docutils literal notranslate"><span class="pre">Group</span></code> are named
<code class="docutils literal notranslate"><span class="pre">mul</span></code>, <code class="docutils literal notranslate"><span class="pre">one</span></code>, and <code class="docutils literal notranslate"><span class="pre">inv</span></code>,
and in a moment we will see how multiplicative notation is
set up to refer to them.
If we want to use additive notation, we instead use an isomorphic structure
<code class="docutils literal notranslate"><span class="pre">AddGroup</span></code> (the structure underlying additive groups). Its components are named <code class="docutils literal notranslate"><span class="pre">add</span></code>, <code class="docutils literal notranslate"><span class="pre">zero</span></code>,
and <code class="docutils literal notranslate"><span class="pre">neg</span></code>, and the associated notation is what you would expect it to be.</p>
<p>Recall the type <code class="docutils literal notranslate"><span class="pre">Point</span></code> that we defined in <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a>,
and the addition function that we defined there.
These definitions are reproduced in the examples file that accompanies
this section.
As an exercise, define an <code class="docutils literal notranslate"><span class="pre">AddGroup&#8321;</span></code> structure that is similar
to the <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> structure we defined above, except that it uses the
additive naming scheme just described.
Define negation and a zero on the <code class="docutils literal notranslate"><span class="pre">Point</span></code> data type,
and define the <code class="docutils literal notranslate"><span class="pre">AddGroup&#8321;</span></code> structure on <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">AddGroup&#8321;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="w">  </span><span class="c1">-- fill in the rest</span>
<span class="kd">@[</span><span class="n">ext</span><span class="kd">]</span>
<span class="kd">structure</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>

<span class="kn">namespace</span><span class="w"> </span><span class="n">Point</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="o">,</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span><span class="o">,</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">neg</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">def</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">def</span><span class="w"> </span><span class="n">addGroupPoint</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">AddGroup&#8321;</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">end</span><span class="w"> </span><span class="n">Point</span>
</pre></div>
</div>
<p>We are making progress.
Now we know how to define algebraic structures in Lean,
and we know how to define instances of those structures.
But we also want to associate notation with structures
so that we can use it with each instance.
Moreover, we want to arrange it so that we can define an operation
on a structure and use it with any particular instance,
and we want to arrange it so that we can prove a theorem about
a structure and use it with any instance.</p>
<p>In fact, Mathlib is already set up to use generic group notation,
definitions, and theorems for <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span>

<span class="c1">-- group power, defined for any group</span>
<span class="k">#check</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">mul_inv_cancel</span><span class="o">,</span><span class="w"> </span><span class="n">mul_one</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mul_inv_cancel_right</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">g.symm.trans</span><span class="w"> </span><span class="o">(</span><span class="n">g.trans</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mul_inv_cancel_right</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span>
</pre></div>
</div>
<p>You can check that this is not the case for the additive group structure
on <code class="docutils literal notranslate"><span class="pre">Point</span></code> that we asked you to define above.
Our task now is to understand that magic that goes on under the hood
in order to make the examples for <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code> work the way they do.</p>
<p>The issue is that Lean needs to be able to <em>find</em> the relevant
notation and the implicit group structure,
using the information that is found in the expressions that we type.
Similarly, when we write <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code> with expressions <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>
that have type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, Lean needs to interpret the <code class="docutils literal notranslate"><span class="pre">+</span></code>
symbol as the relevant addition function on the reals.
It also has to recognize the type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> as an instance of a commutative ring,
so that all the definitions and theorems for a commutative ring are available.
For another example,
continuity is defined in Lean relative to any two topological spaces.
When we have <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8450;</span></code> and we write <code class="docutils literal notranslate"><span class="pre">Continuous</span> <span class="pre">f</span></code>, Lean has to find the
relevant topologies on <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>.</p>
<p>The magic is achieved with a combination of three things.</p>
<ol class="arabic simple">
<li><p><em>Logic.</em> A definition that should be interpreted in any group takes, as
arguments, the type of the group and the group structure as arguments.
Similarly, a theorem about the elements of an arbitrary group
begins with universal quantifiers over
the type of the group and the group structure.</p></li>
<li><p><em>Implicit arguments.</em> The arguments for the type and the structure
are generally left implicit, so that we do not have to write them
or see them in the Lean information window. Lean fills the
information in for us silently.</p></li>
<li><p><em>Type class inference.</em> Also known as <em>class inference</em>,
this is a simple but powerful mechanism
that enables us to register information for Lean to use later on.
When Lean is called on to fill in implicit arguments to a
definition, theorem, or piece of notation,
it can make use of information that has been registered.</p></li>
</ol>
<p>Whereas an annotation <code class="docutils literal notranslate"><span class="pre">(grp</span> <span class="pre">:</span> <span class="pre">Group</span> <span class="pre">G)</span></code> tells Lean that it should
expect to be given that argument explicitly and the annotation
<code class="docutils literal notranslate"><span class="pre">{grp</span> <span class="pre">:</span> <span class="pre">Group</span> <span class="pre">G}</span></code> tells Lean that it should try to figure it out
from contextual cues in the expression,
the annotation <code class="docutils literal notranslate"><span class="pre">[grp</span> <span class="pre">:</span> <span class="pre">Group</span> <span class="pre">G]</span></code> tells Lean that the corresponding
argument should be synthesized using type class inference.
Since the whole point to the use of such arguments is that
we generally do not need to refer to them explicitly,
Lean allows us to write <code class="docutils literal notranslate"><span class="pre">[Group</span> <span class="pre">G]</span></code> and leave the name anonymous.
You have probably already noticed that Lean chooses names like <code class="docutils literal notranslate"><span class="pre">_inst_1</span></code>
automatically.
When we use the anonymous square-bracket annotation with the <code class="docutils literal notranslate"><span class="pre">variables</span></code> command,
then as long as the variables are still in scope,
Lean automatically adds the argument <code class="docutils literal notranslate"><span class="pre">[Group</span> <span class="pre">G]</span></code> to any definition or
theorem that mentions <code class="docutils literal notranslate"><span class="pre">G</span></code>.</p>
<p>How do we register the information that Lean needs to use to carry
out the search?
Returning to our group example, we need only make two changes.
First, instead of using the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command to define the group structure,
we use the keyword <code class="docutils literal notranslate"><span class="pre">class</span></code> to indicate that it is a candidate
for class inference.
Second, instead of defining particular instances with <code class="docutils literal notranslate"><span class="pre">def</span></code>,
we use the keyword <code class="docutils literal notranslate"><span class="pre">instance</span></code> to register the particular instance with
Lean. As with the names of class variables, we are allowed to leave the
name of an instance definition anonymous,
since in general we intend Lean to find it and put it to use
without troubling us with the details.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span><span class="w"> </span><span class="n">Group&#8322;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">inv</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">one</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8322;</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">f</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.symm</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.trans_assoc</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans_refl</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl_trans</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.self_trans_symm</span>
</pre></div>
</div>
<p>The following illustrates their use.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Group&#8322;.mul</span>

<span class="kd">def</span><span class="w"> </span><span class="n">mySquare</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Group&#8322;.mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">x</span>

<span class="k">#check</span><span class="w"> </span><span class="n">mySquare</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#946;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#946;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8322;.mul</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g.trans</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mySquare</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f.trans</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">#check</span></code> command shows that <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span></code> has an implicit argument
<code class="docutils literal notranslate"><span class="pre">[Group&#8322;</span> <span class="pre">&#945;]</span></code> that we expect to be found by class inference,
where <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is the type of the arguments to <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span></code>.
In other words, <code class="docutils literal notranslate"><span class="pre">{&#945;</span> <span class="pre">:</span> <span class="pre">Type*}</span></code> is the implicit argument for the type
of the group elements and <code class="docutils literal notranslate"><span class="pre">[Group&#8322;</span> <span class="pre">&#945;]</span></code> is the implicit argument for the
group structure on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
Similarly, when we define a generic squaring function <code class="docutils literal notranslate"><span class="pre">my_square</span></code>
for <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code>, we use an implicit argument <code class="docutils literal notranslate"><span class="pre">{&#945;</span> <span class="pre">:</span> <span class="pre">Type*}</span></code> for
the type of the elements and an implicit argument <code class="docutils literal notranslate"><span class="pre">[Group&#8322;</span> <span class="pre">&#945;]</span></code> for
the <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code> structure.</p>
<p>In the first example,
when we write <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span> <span class="pre">f</span> <span class="pre">g</span></code>, the type of <code class="docutils literal notranslate"><span class="pre">f</span></code> and <code class="docutils literal notranslate"><span class="pre">g</span></code>
tells Lean that in the argument <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> to <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span></code>
has to be instantiated to <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#946;</span></code>.
That means that Lean has to find an element of <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#946;)</span></code>.
The previous <code class="docutils literal notranslate"><span class="pre">instance</span></code> declaration tells Lean exactly how to do that.
Problem solved!</p>
<p>This simple mechanism for registering information so that Lean can find it
when it needs it is remarkably useful.
Here is one way it comes up.
In Lean&#8217;s foundation, a data type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> may be empty.
In a number of applications, however, it is useful to know that a
type has at least one element.
For example, the function <code class="docutils literal notranslate"><span class="pre">List.headI</span></code>, which returns the first
element of a list, can return the default value when the list is empty.
To make that work, the Lean library defines a class <code class="docutils literal notranslate"><span class="pre">Inhabited</span> <span class="pre">&#945;</span></code>,
which does nothing more than store a default value.
We can show that the <code class="docutils literal notranslate"><span class="pre">Point</span></code> type is an instance:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Inhabited</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span><span class="w"> </span><span class="n">default</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">&#10216;</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">default</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">([]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">List</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="bp">.</span><span class="n">headI</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">default</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>The class inference mechanism is also used for generic notation.
The expression <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code> is an abbreviation for <code class="docutils literal notranslate"><span class="pre">Add.add</span> <span class="pre">x</span> <span class="pre">y</span></code>
where&#8212;you guessed it&#8212;<code class="docutils literal notranslate"><span class="pre">Add</span> <span class="pre">&#945;</span></code> is a class that stores
a binary function on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
Writing <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code> tells Lean to find a registered instance of <code class="docutils literal notranslate"><span class="pre">[Add.add</span> <span class="pre">&#945;]</span></code>
and use the corresponding function.
Below, we register the addition function for <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Add</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Point.add</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Point.add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>In this way, we can assign the notation <code class="docutils literal notranslate"><span class="pre">+</span></code> to binary operations on other
types as well.</p>
<p>But we can do even better. We have seen that <code class="docutils literal notranslate"><span class="pre">*</span></code> can be used in any
group, <code class="docutils literal notranslate"><span class="pre">+</span></code> can be used in any additive group, and both can be used in
any ring.
When we define a new instance of a ring in Lean,
we don&#8217;t have to define <code class="docutils literal notranslate"><span class="pre">+</span></code> and <code class="docutils literal notranslate"><span class="pre">*</span></code> for that instance,
because Lean knows that these are defined for every ring.
We can use this method to specify notation for our <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code> class:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Mul</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">Group&#8322;.mul</span><span class="o">&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">One</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">Group&#8322;.one</span><span class="o">&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Inv</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">Group&#8322;.inv</span><span class="o">&#10217;</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">foo</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g.symm.trans</span><span class="w"> </span><span class="o">((</span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="bp">.</span><span class="n">trans</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>What makes this approach work is that Lean carries out a recursive search.
According to the instances we have declared, Lean can find an instance of
<code class="docutils literal notranslate"><span class="pre">Mul</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code> by finding an
instance of <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code>, and it can find an instance of
<code class="docutils literal notranslate"><span class="pre">Group&#8322;</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code> because we have provided one.
Lean is capable of finding these two facts and chaining them together.</p>
<p>The example we have just given is dangerous, because Lean&#8217;s
library also has an instance of <code class="docutils literal notranslate"><span class="pre">Group</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code>, and
multiplication is defined on any group.
So it is ambiguous as to which instance is found.
In fact, Lean favors more recent declarations unless you explicitly
specify a different priority.
Also, there is another way to tell Lean that one structure is an
instance of another, using the <code class="docutils literal notranslate"><span class="pre">extends</span></code> keyword.
This is how Mathlib specifies that, for example,
every commutative ring is a ring.
You can find more information in <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Section 8</span></a> and in a
<a class="reference external" href="https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#managing-type-class-inference">section on class inference</a> in <em>Theorem Proving in Lean</em>.</p>
<p>In general, it is a bad idea to specify a value of
<code class="docutils literal notranslate"><span class="pre">*</span></code> for an instance of an algebraic structure that already has
the notation defined.
Redefining the notion of <code class="docutils literal notranslate"><span class="pre">Group</span></code> in Lean is an artificial example.
In this case, however, both interpretations of the group notation unfold to
<code class="docutils literal notranslate"><span class="pre">Equiv.trans</span></code>, <code class="docutils literal notranslate"><span class="pre">Equiv.refl</span></code>, and <code class="docutils literal notranslate"><span class="pre">Equiv.symm</span></code>, in the same way.</p>
<p>As a similarly artificial exercise,
define a class <code class="docutils literal notranslate"><span class="pre">AddGroup&#8322;</span></code> in analogy to <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code>.
Define the usual notation for addition, negation, and zero
on any <code class="docutils literal notranslate"><span class="pre">AddGroup&#8322;</span></code>
using the classes <code class="docutils literal notranslate"><span class="pre">Add</span></code>, <code class="docutils literal notranslate"><span class="pre">Neg</span></code>, and <code class="docutils literal notranslate"><span class="pre">Zero</span></code>.
Then show <code class="docutils literal notranslate"><span class="pre">Point</span></code> is an instance of <code class="docutils literal notranslate"><span class="pre">AddGroup&#8322;</span></code>.
Try it out and make sure that the additive group notation works for
elements of <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span><span class="w"> </span><span class="n">AddGroup&#8322;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="c1">-- fill in the rest</span>
</pre></div>
</div>
<p>It is not a big problem that we have already declared instances
<code class="docutils literal notranslate"><span class="pre">Add</span></code>, <code class="docutils literal notranslate"><span class="pre">Neg</span></code>, and <code class="docutils literal notranslate"><span class="pre">Zero</span></code> for <code class="docutils literal notranslate"><span class="pre">Point</span></code> above.
Once again, the two ways of synthesizing the notation should come up
with the same answer.</p>
<p>Class inference is subtle, and you have to be careful when using it,
because it configures automation that invisibly governs the interpretation of
the expressions we type.
When used wisely, however, class inference is a powerful tool.
It is what makes algebraic reasoning possible in Lean.</p>
</section>
<section id="building-the-gaussian-integers">
<span id="section-building-the-gaussian-integers"></span><h2><span class="section-number">7.3. </span>Building the Gaussian Integers<a class="headerlink" href="#building-the-gaussian-integers" title="Link to this heading">&#61633;</a></h2>
<p>We will now illustrate the use of the algebraic hierarchy in Lean by
building an important mathematical object, the <em>Gaussian integers</em>,
and showing that it is a Euclidean domain. In other words, according to
the terminology we have been using, we will define the Gaussian integers
and show that they are an instance of the Euclidean domain structure.</p>
<p>In ordinary mathematical terms, the set of Gaussian integers <span class="math notranslate nohighlight">\(\Bbb{Z}[i]\)</span>
is the set of complex numbers <span class="math notranslate nohighlight">\(\{ a + b i \mid a, b \in \Bbb{Z}\}\)</span>.
But rather than define them as a subset of the complex numbers, our goal
here is to define them as a data type in their own right. We do this by
representing a Gaussian integer as a pair of integers, which we think of as the
<em>real</em> and <em>imaginary</em> parts.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">ext</span><span class="kd">]</span>
<span class="kd">structure</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">re</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span>
<span class="w">  </span><span class="n">im</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span>
</pre></div>
</div>
<p>We first show that the Gaussian integers have the structure of a ring,
with <code class="docutils literal notranslate"><span class="pre">0</span></code> defined to be <code class="docutils literal notranslate"><span class="pre">&#10216;0,</span> <span class="pre">0&#10217;</span></code>, <code class="docutils literal notranslate"><span class="pre">1</span></code> defined to be <code class="docutils literal notranslate"><span class="pre">&#10216;1,</span> <span class="pre">0&#10217;</span></code>, and
addition defined pointwise. To work out the definition of multiplication,
remember that we want the element <span class="math notranslate nohighlight">\(i\)</span>, represented by <code class="docutils literal notranslate"><span class="pre">&#10216;0,</span> <span class="pre">1&#10217;</span></code>, to
be a square root of <span class="math notranslate nohighlight">\(-1\)</span>. Thus we want</p>
<div class="math notranslate nohighlight">
\[\begin{split}(a + bi) (c + di) &amp; = ac + bci + adi + bd i^2 \\
  &amp; = (ac - bd) + (bc + ad)i.\end{split}\]</div>
<p>This explains the definition of <code class="docutils literal notranslate"><span class="pre">Mul</span></code> below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Zero</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;&#10216;</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">One</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;&#10216;</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Add</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.re</span><span class="o">,</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.im</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Neg</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="bp">-</span><span class="n">x.re</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Mul</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">,</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="o">&#10217;&#10217;</span>
</pre></div>
</div>
<p>As noted in <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a>, it is a good idea to put all the definitions
related to a data type in a namespace with the same name. Thus in the Lean
files associated with this chapter, these definitions are made in the
<code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> namespace.</p>
<p>Notice that here we are defining the interpretations of the notation <code class="docutils literal notranslate"><span class="pre">0</span></code>,
<code class="docutils literal notranslate"><span class="pre">1</span></code>, <code class="docutils literal notranslate"><span class="pre">+</span></code>, <code class="docutils literal notranslate"><span class="pre">-</span></code>, and <code class="docutils literal notranslate"><span class="pre">*</span></code> directly, rather than naming them
<code class="docutils literal notranslate"><span class="pre">GaussInt.zero</span></code> and the like and assigning the notation to those.
It is often useful to have an explicit name for the definitions, for example,
to use with <code class="docutils literal notranslate"><span class="pre">simp</span></code> and <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">zero_def</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">one_def</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.re</span><span class="o">,</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.im</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">-</span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="bp">-</span><span class="n">x.re</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">,</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It is also useful to name the rules that compute the real and imaginary
parts, and to declare them to the simplifier.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_re</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_im</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">one_re</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">one_im</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">add_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">add_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">x.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It is now surprisingly easy to show that the Gaussian integers are an instance
of a commutative ring. We are putting the structure concept to good use.
Each particular Gaussian integer is an instance of the <code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> structure,
whereas the type <code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> itself, together with the relevant operations, is an
instance of the <code class="docutils literal notranslate"><span class="pre">CommRing</span></code> structure. The <code class="docutils literal notranslate"><span class="pre">CommRing</span></code> structure, in turn,
extends the notational structures <code class="docutils literal notranslate"><span class="pre">Zero</span></code>, <code class="docutils literal notranslate"><span class="pre">One</span></code>, <code class="docutils literal notranslate"><span class="pre">Add</span></code>,
<code class="docutils literal notranslate"><span class="pre">Neg</span></code>, and <code class="docutils literal notranslate"><span class="pre">Mul</span></code>.</p>
<p>If you type <code class="docutils literal notranslate"><span class="pre">instance</span> <span class="pre">:</span> <span class="pre">CommRing</span> <span class="pre">GaussInt</span> <span class="pre">:=</span> <span class="pre">_</span></code>, click on the light bulb
that appears in VS Code, and then ask Lean to fill in a skeleton for the
structure definition, you will see a scary number of entries.
Jumping to the definition of the structure, however, shows that many of the
fields have default definitions that Lean will fill in for you automatically.
The essential ones appear in the definition below.
A special case are <code class="docutils literal notranslate"><span class="pre">nsmul</span></code> and <code class="docutils literal notranslate"><span class="pre">zsmul</span></code> which should be ignored for now
and will be explained in the next chapter.
In each case, the relevant
identity is proved by unfolding definitions, using the <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic
to reduce the identities to their real and imaginary components,
simplifying, and, if necessary, carrying out the relevant ring calculation in
the integers. Note that we could easily avoid repeating all this code, but
this is not the topic of the current discussion.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="n">instCommRing</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CommRing</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">0</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="n">add</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">  </span><span class="n">neg</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">-</span><span class="n">x</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">  </span><span class="n">nsmul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">nsmulRec</span>
<span class="w">  </span><span class="n">zsmul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">zsmulRec</span>
<span class="w">  </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">zero_add</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">add_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">neg_add_cancel</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">add_comm</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">left_distrib</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">right_distrib</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">mul_comm</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">zero_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">mul_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Lean&#8217;s library defines the class of <em>nontrivial</em> types to be types with at
least two distinct elements. In the context of a ring, this is equivalent
to saying that the zero is not equal to the one. Since some common theorems
depend on that fact, we may as well establish it now.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nontrivial</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Ne</span><span class="o">,</span><span class="w"> </span><span class="n">GaussInt.ext_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>We will now show that the Gaussian integers have an important additional
property. A <em>Euclidean domain</em> is a ring <span class="math notranslate nohighlight">\(R\)</span> equipped with a <em>norm</em>
function <span class="math notranslate nohighlight">\(N : R \to \mathbb{N}\)</span> with the following two properties:</p>
<ul class="simple">
<li><p>For every <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b \ne 0\)</span> in <span class="math notranslate nohighlight">\(R\)</span>, there are
<span class="math notranslate nohighlight">\(q\)</span> and <span class="math notranslate nohighlight">\(r\)</span> in <span class="math notranslate nohighlight">\(R\)</span> such that <span class="math notranslate nohighlight">\(a = bq + r\)</span> and
either <span class="math notranslate nohighlight">\(r = 0\)</span> or <span class="math notranslate nohighlight">\(N(r) &lt; N(b)\)</span>.</p></li>
<li><p>For every <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b \ne 0\)</span>, <span class="math notranslate nohighlight">\(N(a) \le N(ab)\)</span>.</p></li>
</ul>
<p>The ring of integers <span class="math notranslate nohighlight">\(\Bbb{Z}\)</span> with <span class="math notranslate nohighlight">\(N(a) = |a|\)</span> is an
archetypal example of a Euclidean domain.
In that case, we can take <span class="math notranslate nohighlight">\(q\)</span> to be the
result of integer division of <span class="math notranslate nohighlight">\(a\)</span> by <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(r\)</span>
to be the remainder. These functions are defined in Lean so that the
satisfy the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Eq.symm</span><span class="w"> </span><span class="o">(</span><span class="n">Int.ediv_add_emod</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Int.emod_nonneg</span><span class="w"> </span><span class="n">a</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">|</span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Int.emod_lt_abs</span><span class="w"> </span><span class="n">a</span>
</pre></div>
</div>
<p>In an arbitrary ring, an element <span class="math notranslate nohighlight">\(a\)</span> is said to be a <em>unit</em> if it divides
<span class="math notranslate nohighlight">\(1\)</span>. A nonzero element <span class="math notranslate nohighlight">\(a\)</span> is said to be <em>irreducible</em> if it cannot
be written in the form <span class="math notranslate nohighlight">\(a = bc\)</span>
where neither <span class="math notranslate nohighlight">\(b\)</span> nor <span class="math notranslate nohighlight">\(c\)</span> is a unit. In the integers, every
irreducible element <span class="math notranslate nohighlight">\(a\)</span> is <em>prime</em>, which is to say, whenever <span class="math notranslate nohighlight">\(a\)</span>
divides a product <span class="math notranslate nohighlight">\(bc\)</span>, it divides either <span class="math notranslate nohighlight">\(b\)</span> or <span class="math notranslate nohighlight">\(c\)</span>. But
in other rings this property can fail. In the ring
<span class="math notranslate nohighlight">\(\Bbb{Z}[\sqrt{-5}]\)</span>, we have</p>
<div class="math notranslate nohighlight">
\[6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),\]</div>
<p>and the elements <span class="math notranslate nohighlight">\(2\)</span>, <span class="math notranslate nohighlight">\(3\)</span>, <span class="math notranslate nohighlight">\(1 + \sqrt{-5}\)</span>, and
<span class="math notranslate nohighlight">\(1 - \sqrt{-5}\)</span> are all irreducible, but they are not prime. For example,
<span class="math notranslate nohighlight">\(2\)</span> divides the product <span class="math notranslate nohighlight">\((1 + \sqrt{-5})(1 - \sqrt{-5})\)</span>,
but it does not divide either factor. In particular, we no longer have
unique factorization: the number <span class="math notranslate nohighlight">\(6\)</span> can be factored into irreducible
elements in more than one way.</p>
<p>In contrast, every Euclidean domain is a unique factorization domain, which
implies that every irreducible element is prime.
The axioms for a Euclidean domain imply that one can write any nonzero element
as a finite product of irreducible elements. They also imply that one can use
the Euclidean algorithm to find a greatest common divisor of any two
nonzero elements <code class="docutils literal notranslate"><span class="pre">a</span></code> and <code class="docutils literal notranslate"><span class="pre">b</span></code>, i.e. an element that is divisible by any
other common divisor. This, in turn, implies that factorization
into irreducible elements is unique up to multiplication by units.</p>
<p>We now show that the Gaussian integers are a Euclidean domain with
the norm defined by <span class="math notranslate nohighlight">\(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\)</span>.
The Gaussian integer <span class="math notranslate nohighlight">\(a - bi\)</span> is called the <em>conjugate</em> of <span class="math notranslate nohighlight">\(a + bi\)</span>.
It is not hard to check that for any complex numbers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span>,
we have <span class="math notranslate nohighlight">\(N(xy) = N(x)N(y)\)</span>.</p>
<p>To see that this definition of the norm makes the Gaussian integers a Euclidean
domain, only the first property is challenging. Suppose
we want to write <span class="math notranslate nohighlight">\(a + bi = (c + di) q + r\)</span> for suitable <span class="math notranslate nohighlight">\(q\)</span>
and <span class="math notranslate nohighlight">\(r\)</span>. Treating <span class="math notranslate nohighlight">\(a + bi\)</span> and <span class="math notranslate nohighlight">\(c + di\)</span> as complex
numbers, carry out the division</p>
<div class="math notranslate nohighlight">
\[\frac{a + bi}{c + di} = \frac{(a + bi)(c - di)}{(c + di)(c-di)} =
  \frac{ac + bd}{c^2 + d^2} + \frac{bc -ad}{c^2+d^2} i.\]</div>
<p>The real and imaginary parts might not be integers, but we can round
them to the nearest integers <span class="math notranslate nohighlight">\(u\)</span> and <span class="math notranslate nohighlight">\(v\)</span>. We can then express the
right-hand side as <span class="math notranslate nohighlight">\((u + vi) + (u' + v'i)\)</span>, where
<span class="math notranslate nohighlight">\(u' + v'i\)</span> is the part left over. Note that we have
<span class="math notranslate nohighlight">\(|u'| \le 1/2\)</span> and <span class="math notranslate nohighlight">\(|v'| \le 1/2\)</span>, and hence</p>
<div class="math notranslate nohighlight">
\[N(u' + v' i) = (u')^2 + (v')^2 \le 1/4 + 1/4 \le 1/2.\]</div>
<p>Multiplying through by <span class="math notranslate nohighlight">\(c + di\)</span>, we have</p>
<div class="math notranslate nohighlight">
\[a + bi = (c + di) (u + vi) + (c + di) (u' + v'i).\]</div>
<p>Setting <span class="math notranslate nohighlight">\(q = u + vi\)</span> and <span class="math notranslate nohighlight">\(r = (c + di) (u' + v'i)\)</span>, we have
<span class="math notranslate nohighlight">\(a + bi = (c + di) q + r\)</span>, and we only need to
bound <span class="math notranslate nohighlight">\(N(r)\)</span>:</p>
<div class="math notranslate nohighlight">
\[N(r) = N(c + di)N(u' + v'i) \le N(c + di) \cdot 1/2 &lt; N(c + di).\]</div>
<p>The argument we just carried out requires viewing the Gaussian integers
as a subset of the complex numbers. One option for formalizing it in Lean
is therefore to embed the Gaussian integers in the complex numbers, embed
the integers in the Gaussian integers, define the rounding function from the
real numbers to the integers, and take great care to pass back and forth
between these number systems appropriately.
In fact, this is exactly the approach that is followed in Mathlib,
where the Gaussian integers themselves are constructed as a special case
of a ring of <em>quadratic integers</em>.
See the file <a class="reference external" href="https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean">GaussianInt.lean</a>.</p>
<p>Here we will instead carry out an argument that stays in the integers.
This illustrates a choice one commonly faces when formalizing mathematics.
Given an argument that requires concepts or machinery that is not already
in the library, one has two choices: either formalize the concepts and machinery
needed, or adapt the argument to make use of concepts and machinery you
already have.
The first choice is generally a good investment of time when the results
can be used in other contexts.
Pragmatically speaking, however, sometimes seeking a more elementary proof
is more efficient.</p>
<p>The usual quotient-remainder theorem for the integers says that for
every <span class="math notranslate nohighlight">\(a\)</span> and nonzero <span class="math notranslate nohighlight">\(b\)</span>, there are <span class="math notranslate nohighlight">\(q\)</span> and <span class="math notranslate nohighlight">\(r\)</span>
such that <span class="math notranslate nohighlight">\(a = b q + r\)</span> and <span class="math notranslate nohighlight">\(0 \le r &lt; b\)</span>.
Here we will make use of the following variation, which says that there
are <span class="math notranslate nohighlight">\(q'\)</span> and <span class="math notranslate nohighlight">\(r'\)</span> such that
<span class="math notranslate nohighlight">\(a = b q' + r'\)</span> and <span class="math notranslate nohighlight">\(|r'| \le b/2\)</span>.
You can check that if the value of <span class="math notranslate nohighlight">\(r\)</span> in the first statement
satisfies <span class="math notranslate nohighlight">\(r \le b/2\)</span>, we can take <span class="math notranslate nohighlight">\(q' = q\)</span> and <span class="math notranslate nohighlight">\(r' = r\)</span>,
and otherwise we can take <span class="math notranslate nohighlight">\(q' = q + 1\)</span> and <span class="math notranslate nohighlight">\(r' = r - b\)</span>.
We are grateful to Heather Macbeth for suggesting the following more
elegant approach, which avoids definition by cases.
We simply add <code class="docutils literal notranslate"><span class="pre">b</span> <span class="pre">/</span> <span class="pre">2</span></code> to <code class="docutils literal notranslate"><span class="pre">a</span></code> before dividing and then subtract it
from the remainder.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">b</span>

<span class="kd">def</span><span class="w"> </span><span class="n">mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">div&#39;_add_mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">div&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">div&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">mod&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">Int.ediv_add_emod</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">b</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">abs_mod&#39;_le</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">|</span><span class="n">mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mod&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">abs_le</span><span class="o">]</span>
<span class="w">  </span><span class="n">constructor</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">Int.emod_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">h.ne&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.emod_lt_of_pos</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.ediv_add_emod</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.emod_lt_of_pos</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">zero_lt_two</span>
<span class="w">  </span><span class="n">linarith</span>
</pre></div>
</div>
<p>Note the use of our old friend, <code class="docutils literal notranslate"><span class="pre">linarith</span></code>. We will also need to express
<code class="docutils literal notranslate"><span class="pre">mod'</span></code> in terms of <code class="docutils literal notranslate"><span class="pre">div'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">mod&#39;_eq</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">div&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">div&#39;_add_mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">]</span>
</pre></div>
</div>
<p>We will use the fact that <span class="math notranslate nohighlight">\(x^2 + y^2\)</span> is equal to zero if and only if
<span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are both zero. As an exercise, we ask you to prove
that this holds in any ordered ring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sq_add_sq_eq_zero</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">LinearOrder</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsStrictOrderedRing</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We will put all the remaining definitions and theorems in this section
in the <code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> namespace.
First, we define the <code class="docutils literal notranslate"><span class="pre">norm</span></code> function and ask you to establish
some of its properties.
The proofs are all short.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">x.re</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_eq_zero</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_pos</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_mul</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Next we define the conjugate function:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="o">&#10217;</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">conj_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">conj</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">conj_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">conj</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_conj</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">conj</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">norm</span><span class="o">]</span>
</pre></div>
</div>
<p>Finally, we define division for the Gaussian integers
with the notation <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code>, that rounds the complex quotient to the nearest
Gaussian integer. We use our bespoke <code class="docutils literal notranslate"><span class="pre">Int.div'</span></code> for that purpose.
As we calculated above, if <code class="docutils literal notranslate"><span class="pre">x</span></code> is <span class="math notranslate nohighlight">\(a + bi\)</span> and <code class="docutils literal notranslate"><span class="pre">y</span></code> is <span class="math notranslate nohighlight">\(c + di\)</span>,
then the real and imaginary parts of <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code> are the nearest integers to</p>
<div class="math notranslate nohighlight">
\[\frac{ac + bd}{c^2 + d^2} \quad \text{and} \quad \frac{bc -ad}{c^2+d^2},\]</div>
<p>respectively. Here the numerators are the real and imaginary parts of
<span class="math notranslate nohighlight">\((a + bi) (c - di)\)</span>, and the denominators are both equal to the norm
of <span class="math notranslate nohighlight">\(c + di\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Div</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">),</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;&#10217;</span>
</pre></div>
</div>
<p>Having defined <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code>, We define <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">%</span> <span class="pre">y</span></code> to be the remainder,
<code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">-</span> <span class="pre">(x</span> <span class="pre">/</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">y</span></code>. As above, we record the definitions in the
theorems <code class="docutils literal notranslate"><span class="pre">div_def</span></code> and
<code class="docutils literal notranslate"><span class="pre">mod_def</span></code> so that we can use them with <code class="docutils literal notranslate"><span class="pre">simp</span></code> and <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Mod</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">div_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">),</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mod_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>These definitions immediately yield <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">=</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">(x</span> <span class="pre">/</span> <span class="pre">y)</span> <span class="pre">+</span> <span class="pre">x</span> <span class="pre">%</span> <span class="pre">y</span></code> for every
<code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>, so all we need to do is show that the norm of <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">%</span> <span class="pre">y</span></code> is
less than the norm of <code class="docutils literal notranslate"><span class="pre">y</span></code> when <code class="docutils literal notranslate"><span class="pre">y</span></code> is not zero.</p>
<p>We just defined the real and imaginary parts of <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code> to be
<code class="docutils literal notranslate"><span class="pre">div'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).re</span> <span class="pre">(norm</span> <span class="pre">y)</span></code> and <code class="docutils literal notranslate"><span class="pre">div'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).im</span> <span class="pre">(norm</span> <span class="pre">y)</span></code>,
respectively.
Calculating, we have</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">(x</span> <span class="pre">-</span> <span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y</span> <span class="pre">-</span> <span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">(y</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y)</span></code></p>
</div></blockquote>
<p>The real and imaginary parts of the right-hand side are exactly <code class="docutils literal notranslate"><span class="pre">mod'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).re</span> <span class="pre">(norm</span> <span class="pre">y)</span></code> and <code class="docutils literal notranslate"><span class="pre">mod'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).im</span> <span class="pre">(norm</span> <span class="pre">y)</span></code>.
By the properties of <code class="docutils literal notranslate"><span class="pre">div'</span></code> and <code class="docutils literal notranslate"><span class="pre">mod'</span></code>,
these are guaranteed to be less than or equal to <code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2</span></code>.
So we have</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">((x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y)</span> <span class="pre">&#8804;</span> <span class="pre">(norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2)^2</span> <span class="pre">+</span> <span class="pre">(norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2)^2</span> <span class="pre">&#8804;</span> <span class="pre">(norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2)</span> <span class="pre">*</span> <span class="pre">norm</span> <span class="pre">y</span></code>.</p>
</div></blockquote>
<p>On the other hand, we have</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">((x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y)</span> <span class="pre">=</span> <span class="pre">norm</span> <span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">norm</span> <span class="pre">(conj</span> <span class="pre">y)</span> <span class="pre">=</span> <span class="pre">norm</span> <span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">norm</span> <span class="pre">y</span></code>.</p>
</div></blockquote>
<p>Dividing through by <code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">y</span></code> we have <code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">&#8804;</span> <span class="pre">(norm</span> <span class="pre">y)</span> <span class="pre">/</span> <span class="pre">2</span> <span class="pre">&lt;</span> <span class="pre">norm</span> <span class="pre">y</span></code>,
as required.</p>
<p>This messy calculation is carried out in the next proof. We encourage you
to step through the details and see if you can find a nicer argument.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">norm_mod_lt</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">norm</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y.norm</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">norm_y_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rwa</span><span class="w"> </span><span class="o">[</span><span class="n">norm_pos</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">H1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">),</span><span class="w"> </span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Int.mod&#39;_eq</span><span class="o">,</span><span class="w"> </span><span class="n">mod_def</span><span class="o">,</span><span class="w"> </span><span class="n">div_def</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">]</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">H2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="k">calc</span>
<span class="w">      </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">norm_mul</span><span class="o">,</span><span class="w"> </span><span class="n">norm_conj</span><span class="o">]</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">|</span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">|</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span>
<span class="w">          </span><span class="bp">+</span><span class="w"> </span><span class="bp">|</span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="o">(</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">|</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">H1</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">,</span><span class="w"> </span><span class="n">sq_abs</span><span class="o">]</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="o">(</span><span class="n">y.norm</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">y.norm</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">gcongr</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.abs_mod&#39;_le</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">norm_y_pos</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">gcongr</span><span class="bp">;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ediv_mul_le</span><span class="bp">;</span><span class="w"> </span><span class="n">norm_num</span>
<span class="w">  </span><span class="k">calc</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">le_of_mul_le_mul_right</span><span class="w"> </span><span class="n">H2</span><span class="w"> </span><span class="n">norm_y_pos</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">        </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ediv_lt_of_lt_mul</span>
<span class="w">        </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">norm_num</span>
<span class="w">        </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">linarith</span>
</pre></div>
</div>
<p>We are in the home stretch. Our <code class="docutils literal notranslate"><span class="pre">norm</span></code> function maps Gaussian integers to
nonnegative integers. We need a function that maps Gaussian integers to natural
numbers, and we obtain that by composing <code class="docutils literal notranslate"><span class="pre">norm</span></code> with the function
<code class="docutils literal notranslate"><span class="pre">Int.natAbs</span></code>, which maps integers to the natural numbers.
The first of the next two lemmas establishes that mapping the norm to the
natural numbers and back to the integers does not change the value.
The second one re-expresses the fact that the norm is decreasing.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">coe_natAbs_norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x.norm.natAbs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.norm</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Int.natAbs_of_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">norm_nonneg</span><span class="w"> </span><span class="n">_</span><span class="o">)</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">natAbs_norm_mod_lt</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">norm.natAbs</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y.norm.natAbs</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ofNat_lt</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">Int.natCast_natAbs</span><span class="o">,</span><span class="w"> </span><span class="n">abs_of_nonneg</span><span class="o">,</span><span class="w"> </span><span class="n">norm_nonneg</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">norm_mod_lt</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">hy</span>
</pre></div>
</div>
<p>We also need to establish the second key property of the norm function
on a Euclidean domain.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">not_norm_mul_left_lt_norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#172;</span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">))</span><span class="bp">.</span><span class="n">natAbs</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">natAbs</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">not_lt_of_ge</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">norm_mul</span><span class="o">,</span><span class="w"> </span><span class="n">Int.natAbs_mul</span><span class="o">]</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_mul_of_one_le_right</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.zero_le</span><span class="w"> </span><span class="n">_</span><span class="o">)</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ofNat_le</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">coe_natAbs_norm</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">Int.add_one_le_of_lt</span><span class="w"> </span><span class="o">((</span><span class="n">norm_pos</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="bp">.</span><span class="n">mpr</span><span class="w"> </span><span class="n">hy</span><span class="o">)</span>
</pre></div>
</div>
<p>We can now put it together to show that the Gaussian integers are an
instance of a Euclidean domain. We use the quotient and remainder function we
have defined.
The Mathlib definition of a Euclidean domain is more general than the one
above in that it allows us to show that remainder decreases with respect
to any well-founded measure.
Comparing the values of a norm function that returns natural numbers is
just one instance of such a measure,
and in that case, the required properties are the theorems
<code class="docutils literal notranslate"><span class="pre">natAbs_norm_mod_lt</span></code> and <code class="docutils literal notranslate"><span class="pre">not_norm_mul_left_lt_norm</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">EuclideanDomain</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">GaussInt.instCommRing</span><span class="w"> </span><span class="k">with</span>
<span class="w">    </span><span class="n">quotient</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">    </span><span class="n">remainder</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">    </span><span class="n">quotient_mul_add_remainder_eq</span><span class="w"> </span><span class="o">:=</span>
<span class="w">      </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mod_def</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">]</span><span class="w"> </span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">    </span><span class="n">quotient_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">div_def</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">,</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="o">]</span>
<span class="w">      </span><span class="n">rfl</span>
<span class="w">    </span><span class="n">r</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">measure</span><span class="w"> </span><span class="o">(</span><span class="n">Int.natAbs</span><span class="w"> </span><span class="bp">&#8728;</span><span class="w"> </span><span class="n">norm</span><span class="o">))</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">    </span><span class="n">r_wellFounded</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">measure</span><span class="w"> </span><span class="o">(</span><span class="n">Int.natAbs</span><span class="w"> </span><span class="bp">&#8728;</span><span class="w"> </span><span class="n">norm</span><span class="o">))</span><span class="bp">.</span><span class="mi">2</span>
<span class="w">    </span><span class="n">remainder_lt</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">natAbs_norm_mod_lt</span>
<span class="w">    </span><span class="n">mul_left_not_lt</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">not_norm_mul_left_lt_norm</span><span class="w"> </span><span class="o">}</span>
</pre></div>
</div>
<p>An immediate payoff is that we now know that, in the Gaussian integers,
the notions of being prime and being irreducible coincide.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Irreducible</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Prime</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">irreducible_iff_prime</span>
</pre></div>
</div>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C06_Discrete_Mathematics.html" class="btn btn-neutral float-left" title="6. Discrete Mathematics" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C08_Hierarchies.html" class="btn btn-neutral float-right" title="8. Hierarchies" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>